package typechecker.walkers;

import java.util.Set;
import java.util.Vector;

import typechecker.Stage;
import typechecker.ast.type.ForallType;
import typechecker.ast.type.FunctionType;
import typechecker.ast.type.TypeConstructor;
import typechecker.ast.type.TypeConstructorApplication;
import typechecker.ast.type.TypeExpression;
import typechecker.ast.type.TypeVariable;

/**
 * Replace inference stage variables found in 'v', with
 * their succesor. A new type expression is built.
 */
public class TypeSucc {	
	
	private static TypeExpression succConstructorApplication(
			TypeConstructorApplication te, Set<Integer> v) {
		TypeConstructor tc = te.getCons();
		Stage tcStage = tc.getStage();
		int stageNr = tcStage.getIndexOfInferenceVar();
		
		if( v.contains(stageNr)){
			tc.setStage(tcStage.succ());
		}

		Vector<TypeExpression> paramsSucc = new Vector<TypeExpression>(te.getParams().size());
		for( TypeExpression param : te.getParams()){
			paramsSucc.add(succ(param, v));
		}

		return new TypeConstructorApplication(tc, paramsSucc);
	}

	private static TypeExpression succFunctionType(FunctionType te, Set<Integer> v) {
		return new FunctionType( succ(te.getSrc() , v) , succ( te.getDest(), v) );
	}

	private static TypeExpression succForallType(ForallType te, Set<Integer> v) {
		return new ForallType(te.getQuant(), succ(te.getBody(), v));
	}

	private static TypeExpression succVariable(TypeVariable te, Set<Integer> v) {
		return te;
	}

	public static TypeExpression succ(TypeExpression te, Set<Integer> v){
		if (te instanceof ForallType){
			return succForallType((ForallType)te, v);
		} else if ( te instanceof FunctionType){
			return succFunctionType((FunctionType)te, v);
		} else if ( te instanceof TypeConstructorApplication){
			return succConstructorApplication((TypeConstructorApplication) te, v);
		} else if ( te instanceof TypeVariable){
			return succVariable((TypeVariable)te, v);
		}
		return null;
	}
}

